\begin{tabbing}
st{-}key{-}match(${\it tab}$;$k_{1}$;$k_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Case $k_{1}$ of\+
\\[0ex]inl($n$) $\Rightarrow$ \=Case $k_{2}$ of\+
\\[0ex]inl($m$) $\Rightarrow$ false$_{2}$
\\[0ex]inr($a$) $\Rightarrow$ $n$$<_{2}$ptr(${\it tab}$) $\wedge_{2}$ $n$$<_{2}\parallel$${\it tab}$$\parallel$  $\wedge_{2}$ eq\_atom1(st{-}atom(${\it tab}$;$n$);$a$)
\-\\[0ex]inr($a$) $\Rightarrow$ \=Case $k_{2}$ of\+
\\[0ex]inl($n$) $\Rightarrow$ $n$$<_{2}$ptr(${\it tab}$) $\wedge_{2}$ $n$$<_{2}\parallel$${\it tab}$$\parallel$  $\wedge_{2}$ eq\_atom1(st{-}atom(${\it tab}$;$n$);$a$)
\\[0ex]inr($b$) $\Rightarrow$ false$_{2}$
\-\-
\end{tabbing}